/-
Copyright (c) 2020 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import algebra.lie.of_associative
import algebra.ring_quot
import linear_algebra.tensor_algebra.basic

/-!
# Universal enveloping algebra

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

Given a commutative ring `R` and a Lie algebra `L` over `R`, we construct the universal
enveloping algebra of `L`, together with its universal property.

## Main definitions

  * `universal_enveloping_algebra`: the universal enveloping algebra, endowed with an
    `R`-algebra structure.
  * `universal_enveloping_algebra.ι`: the Lie algebra morphism from `L` to its universal
    enveloping algebra.
  * `universal_enveloping_algebra.lift`: given an associative algebra `A`, together with a Lie
    algebra morphism `f : L →ₗ⁅R⁆ A`, `lift R L f : universal_enveloping_algebra R L →ₐ[R] A` is the
    unique morphism of algebras through which `f` factors.
  * `universal_enveloping_algebra.ι_comp_lift`: states that the lift of a morphism is indeed part
    of a factorisation.
  * `universal_enveloping_algebra.lift_unique`: states that lifts of morphisms are indeed unique.
  * `universal_enveloping_algebra.hom_ext`: a restatement of `lift_unique` as an extensionality
    lemma.

## Tags

lie algebra, universal enveloping algebra, tensor algebra
-/

universes u₁ u₂ u₃

variables (R : Type u₁) (L : Type u₂)
variables [comm_ring R] [lie_ring L] [lie_algebra R L]

local notation `ιₜ` := tensor_algebra.ι R

namespace universal_enveloping_algebra

/-- The quotient by the ideal generated by this relation is the universal enveloping algebra.

Note that we have avoided using the more natural expression:
| lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆) ⁅ιₜ x, ιₜ y⁆
so that our construction needs only the semiring structure of the tensor algebra. -/
inductive rel : tensor_algebra R L → tensor_algebra R L → Prop
| lie_compat (x y : L) : rel (ιₜ ⁅x, y⁆ + (ιₜ y) * (ιₜ x)) ((ιₜ x) * (ιₜ y))

end universal_enveloping_algebra

/-- The universal enveloping algebra of a Lie algebra. -/
@[derive [inhabited, ring, algebra R]]
def universal_enveloping_algebra := ring_quot (universal_enveloping_algebra.rel R L)

namespace universal_enveloping_algebra

/-- The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of
associative algebras. -/
def mk_alg_hom : tensor_algebra R L →ₐ[R] universal_enveloping_algebra R L :=
ring_quot.mk_alg_hom R (rel R L)

variables {L}

/-- The natural Lie algebra morphism from a Lie algebra to its universal enveloping algebra. -/
def ι : L →ₗ⁅R⁆ universal_enveloping_algebra R L :=
{ map_lie'   := λ x y, by
  { suffices : mk_alg_hom R L (ιₜ ⁅x, y⁆ + (ιₜ y) * (ιₜ x)) = mk_alg_hom R L ((ιₜ x) * (ιₜ y)),
    { rw alg_hom.map_mul at this, simp [lie_ring.of_associative_ring_bracket, ← this], },
    exact ring_quot.mk_alg_hom_rel _ (rel.lie_compat x y), },
  ..(mk_alg_hom R L).to_linear_map.comp ιₜ }

variables {A : Type u₃} [ring A] [algebra R A] (f : L →ₗ⁅R⁆ A)

/-- The universal property of the universal enveloping algebra: Lie algebra morphisms into
associative algebras lift to associative algebra morphisms from the universal enveloping algebra. -/
def lift : (L →ₗ⁅R⁆ A) ≃ (universal_enveloping_algebra R L →ₐ[R] A) :=
{ to_fun := λ f,
    ring_quot.lift_alg_hom R ⟨tensor_algebra.lift R (f : L →ₗ[R] A),
    begin
      intros a b h, induction h with x y,
      simp only [lie_ring.of_associative_ring_bracket,
        map_add, tensor_algebra.lift_ι_apply, lie_hom.coe_to_linear_map, lie_hom.map_lie,
        map_mul, sub_add_cancel],
    end⟩,
  inv_fun := λ F, (F : universal_enveloping_algebra R L →ₗ⁅R⁆ A).comp (ι R),
  left_inv := λ f, by { ext, simp only [ι, mk_alg_hom,
    tensor_algebra.lift_ι_apply, lie_hom.coe_to_linear_map, linear_map.to_fun_eq_coe,
    linear_map.coe_comp, lie_hom.coe_comp, alg_hom.coe_to_lie_hom, lie_hom.coe_mk,
    function.comp_app, alg_hom.to_linear_map_apply, ring_quot.lift_alg_hom_mk_alg_hom_apply], },
  right_inv := λ F, by { ext, simp only [ι, mk_alg_hom,
    tensor_algebra.lift_ι_apply, lie_hom.coe_to_linear_map, linear_map.to_fun_eq_coe,
    linear_map.coe_comp, lie_hom.coe_linear_map_comp, alg_hom.comp_to_linear_map,
    function.comp_app, alg_hom.to_linear_map_apply, ring_quot.lift_alg_hom_mk_alg_hom_apply,
    alg_hom.coe_to_lie_hom, lie_hom.coe_mk], } }

@[simp] lemma lift_symm_apply (F : universal_enveloping_algebra R L →ₐ[R] A) :
  (lift R).symm F = (F : universal_enveloping_algebra R L →ₗ⁅R⁆ A).comp (ι R) :=
rfl

@[simp] lemma ι_comp_lift : (lift R f) ∘ (ι R) = f :=
funext $ lie_hom.ext_iff.mp $ (lift R).symm_apply_apply f

@[simp] lemma lift_ι_apply (x : L) : lift R f (ι R x) = f x :=
by rw [←function.comp_apply (lift R f) (ι R) x, ι_comp_lift]

lemma lift_unique (g : universal_enveloping_algebra R L →ₐ[R] A) :
  g ∘ (ι R) = f ↔ g = lift R f :=
begin
  refine iff.trans _ (lift R).symm_apply_eq,
  split; {intro h, ext, simp [←h] },
end

/-- See note [partially-applied ext lemmas]. -/
@[ext] lemma hom_ext {g₁ g₂ : universal_enveloping_algebra R L →ₐ[R] A}
  (h : (g₁ : universal_enveloping_algebra R L →ₗ⁅R⁆ A).comp (ι R) =
       (g₂ : universal_enveloping_algebra R L →ₗ⁅R⁆ A).comp (ι R)) :
  g₁ = g₂ :=
have h' : (lift R).symm g₁ = (lift R).symm g₂, { ext, simp [h], },
(lift R).symm.injective h'

end universal_enveloping_algebra
